%\chapter{Proof of Lemma \ref{l:corr_minsky}}
%\label{s:app_minsky}

%Let us recall the statement of the Lemma, concerning 
%This appendix is devoted to the proof of correctness of the encoding of Minsky machines into \ahopi. 

We now proceed with the proofs. 
In what follows we assume a Minsky machine $N$ with instructions $(1:I_1), \ldots, (n:I_n)$
and with registers $r_0 = m_0$ and $r_1 = m_1$. The encoding of a  configuration $(i, m_0, m_1)$ of $N$ is 
denoted $\encp{(i, m_0, m_1)_N}{\mms}$. We use $\pired^j$ to stand for
%the transitive closure of $\pired$.
a sequence of $j$ reductions.

\begin{mylem}\label{l:sound} 
Let $(i, m_0, m_1)$ be a configuration of a  Minsky machine $N$. \\
If $(i, m_0, m_1) \minskred (i', m'_0, m'_1)$ then there exist a finite $j$ and a process $P$ such that \\
$\encp{(i, m_0, m_1)_N}{\mms} \pired^j P$ and $P = \encp{(i', m'_0, m'_1)_N}{\mms}$.
\end{mylem} 

\begin{proof}
We proceed by case analysis on the instruction performed by the Minsky machine. 
Hence, we distinguish three cases corresponding to the behaviors associated to rules 
\textsc{M-Jmp}, \textsc{M-Dec}, and \textsc{M-Inc}.
%All cases are similar; an extra transition is needed in the case an instruction  $\mathtt{DECJ}$ is involved.

\paragraph{Case \textsc{M-Jmp}} 
We have a Minsky configuration $(i, m_0, m_1)$ with $m_0 = 0$ and $(i: \mathtt{DECJ}(r_0,k))$. 
By Definition \ref{encod-conf}, its encoding in \ahopi is as follows:
\begin{eqnarray*}
\encp{(i, m_0, m_1)_N}{\mms} & = & \overline{p_i} \parallel \encp{r_0 = 0}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel \\ 
& & \encp{(i: \mathtt{DECJ}(r_0,k))}{\mms} \parallel \prod_{l = 1..n, l \not = i} \encp{(l : I_l)}{\mms}
\end{eqnarray*}
We begin by noting that the program counter $p_i$ is consumed by the encoding of the instruction $i$. 
The content of the instruction is thus exposed, and we then have  
\[
\encp{(i, m_0, m_1)_N}{\mms} \pired \encp{r_0 = 0}{\mms} \parallel  \choice{dec_0} \parallel ack.(z_0.\overline{p_k} + n_0.\overline{p_{i+1}}) \parallel S = P_1 
\]
where $S = \encp{r_1 = m_1}{\mms} \parallel \prod^{n}_{l = 1} \encp{(l : I_l)}{\mms}$ stands for the rest of the system.
The only transition possible at this point is the behavior selection on $dec_0$,
which yields the following:
\[
P_1 \pired \overline{r_0^0} \parallel  \choice{z_0} \parallel \mathsf{REG}_0  \parallel ack.(z_0.\overline{p_k} + n_0.\overline{p_{i+1}}) \parallel S = P_2
\]
Now there is a synchronization between $\overline{r_0^0}$ and $\mathsf{REG}_0$ for reconstructing the register
\begin{eqnarray*}
P_2 & \pired   & \choice{z_0}  \parallel \overline{ack} \parallel (inc_0.\out{r_0^\mathsf{S}}{\encn{0}{0}} \, + \, dec_0.(\overline{r_0^0}  \parallel  \choice{z_0})) \parallel \mathsf{REG}_0  \parallel \\
& & ack.(z_0.\overline{p_k} + n_0.\overline{p_{i+1}}) \parallel S = P_3
\end{eqnarray*}
Once the register has been re-created, register and instruction can now synchronize on $ack$: 
\begin{eqnarray*}
P_3 & \pired   & \choice{z_0}  \parallel (inc_0.\out{r_0^\mathsf{S}}{\encn{0}{0}} \, + \, dec_0.(\overline{r_0^0}  \parallel  \choice{z_0})) \parallel \mathsf{REG}_0  \parallel \\
& & z_0.\overline{p_k} + n_0.\overline{p_{i+1}} \parallel S = P_4
\end{eqnarray*}
At this point, the only possible transition  is the behavior selection on $z_0$, which indicates 
that the content of $r_0$ was indeed zero:
\[
P_4 \pired     (inc_0.\out{r_0^\mathsf{S}}{\encn{0}{0}} \, + \, dec_0.(\overline{r_0^0}  \parallel  \choice{z_0})) \parallel \mathsf{REG}_0  \parallel \overline{p_k} \parallel S = P_5
\]
Using the definitions of $\encp{\cdot}{\mms}$ and $S$, and some reordering,
 we note that $P_5$ can be equivalently written as 
\[
P_5 = \overline{p_k} \parallel \encp{r_0 = 0}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel \prod^{n}_{l = 1} \encp{(l : I_l)}{\mms}
\]
which, in turn, corresponds to the encoding of $\encp{(k,0,m_1)_N}{\mms}$, as desired.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\paragraph{Case \textsc{M-Dec}}  %Similar to the previous case.

We have a Minsky configuration $(i, m_0, m_1)$ with $m_0 = c$ (for some $c >0$) and $(i: \mathtt{DECJ}(r_0,k))$. 
By Definition \ref{encod-conf}, its encoding in \ahopi is as follows:
\begin{eqnarray*}
\encp{(i, m_0, m_1)_N}{\mms} &=& \overline{p_i} \parallel \encp{r_0 = c}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel \\ 
& & \encp{(i: \mathtt{DECJ}(r_0,k))}{\mms} \parallel \prod_{l = 1..n, l \not = i} \encp{(l : I_l)}{\mms}
\end{eqnarray*}
We begin by noting that the program counter $p_i$ is consumed by the encoding of the instruction $i$. 
The content of the instruction is thus exposed, and we then have  
\[
\encp{(i, m_0, m_1)_N}{\mms} \pired \encp{r_0 = c}{\mms} \parallel  \choice{dec_0} \parallel ack.(z_0.\overline{p_k} + n_0.\overline{p_{i+1}}) \parallel S = P_1 
\]
where $S = \encp{r_1 = m_1}{\mms} \parallel \prod^{n}_{l = 1} \encp{(l : I_l)}{\mms}$ stands for the rest of the system.
The only transition possible at this point is the behavior selection on $dec_0$,
which yields the following:
\[
P_1 \pired %\out{r_0^\mathsf{S}}{\encn{c}{0}}  
\encn{c-1}{0}  \parallel \mathsf{REG}_0  \parallel ack.(z_0.\overline{p_k} + n_0.\overline{p_{i+1}}) \parallel S = P_2
\]
 
It is worth recalling that $\encn{c-1}{0} = \out{r_0^\mathsf{S}}{\encn{c-2}{0}} \parallel \choice{n_0}$.
Considering this, now there is a synchronization between $\overline{r_0^\mathsf{S}}$ and $\mathsf{REG}_0$ for decrementing the value of the register
\begin{eqnarray*}
P_2 & \pired   &  \choice{n_0} \parallel \overline{ack} \parallel (inc_0.(\out{r_0^\mathsf{S}}{\encn{c-1}{0}} \parallel \choice{n_0}) \, + \, dec_0.\encn{c-2}{0}) \parallel \mathsf{REG}_0  \parallel \\
& & ack.(z_0.\overline{p_k} + n_0.\overline{p_{i+1}}) \parallel S = P_3
\end{eqnarray*}
Once the register has been re-created, register and instruction can now synchronize on $ack$: 
\begin{eqnarray*}
P_3 & \pired   & \choice{n_0}  \parallel (inc_0.(\out{r_0^\mathsf{S}}{\encn{c-1}{0}} \parallel \choice{n_0})\, + \, dec_0.\encn{c-2}{0}) \parallel \mathsf{REG}_0  \parallel \\
& & z_0.\overline{p_k} + n_0.\overline{p_{i+1}} \parallel S = P_4
\end{eqnarray*}
At this point, the only possible transition  is the behavior selection on $n_0$, which indicates 
that the content of $r_0$ was greater than zero:
\[
P_4 \pired     (inc_0.(\out{r_0^\mathsf{S}}{\encn{c-1}{0}} \parallel \choice{n_0}) \, + \, dec_0.\encn{c-2}{0}) \parallel \mathsf{REG}_0  \parallel \overline{p_{i+1}} \parallel S = P_5
\]
Using the definitions of $\encp{\cdot}{\mms}$ and $S$, and some reordering,
 we note that $P_5$ can be equivalently written as 
\[
P_5 = \overline{p_{i+1}} \parallel \encp{r_0 = c-1}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel \prod^{n}_{l = 1} \encp{(l : I_l)}{\mms}
\]
which, in turn, corresponds to the encoding of $\encp{(i+1,c-1,m_1)_N}{\mms}$, as desired.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\paragraph{Case \textsc{M-Inc}} 
We have a Minsky configuration $(i, m_0, m_1)$ with $(i: \mathtt{INC}(r_0))$. 
Its encoding in \ahopi is as follows:
\begin{eqnarray*}
\encp{(i, m_0, m_1)_N}{\mms} & = & \overline{p_i} \parallel \encp{r_0 = m_0}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel \\ 
& & \encp{(i: \mathtt{INC}(r_0))}{\mms} \parallel \prod_{l = 1..n, l \not = i} \encp{(l : I_l)}{\mms}
\end{eqnarray*}
We begin by noting that the program counter $p_i$ is consumed by the encoding of the instruction $i$: %. We then have  
\[
\encp{(i, m_0, m_1)_N}{\mms} \pired \encp{r_0 = m_0}{\mms} \parallel  \choice{inc_0} \parallel ack.\overline{p_{i+1}} \parallel S = P_1 
\]
where $S = \encp{r_1 = m_1}{\mms} \parallel \prod^{n}_{l = 1} \encp{(l : I_l)}{\mms}$ stands for the rest of the system.
The only transition possible at this point is the behavior selection on $inc_0$. After such a selection we have
\[
P_1 \pired \out{r_0^\mathsf{S}}{\encn{m_0}{0}}  \parallel \mathsf{REG}_0  \parallel ack.\overline{p_{i+1}} \parallel S = P_2
\]

Now there is a synchronization between $\overline{r_0^\mathsf{S}}$ and $\mathsf{REG}_0$ for incrementing the value of the register
\begin{eqnarray*}
P_2 & \pired   &  \overline{ack} \parallel (inc_0.(\out{r_0^\mathsf{S}}{\out{r_0^\mathsf{S}}{\encn{m_0}{0}} \parallel \choice{n_0}}) \, + \, dec_0.(\encn{m_0}{0})) \parallel \mathsf{REG}_0  \parallel \\
& & ack.\overline{p_{i+1}} \parallel S = P_3
\end{eqnarray*}
Once the register has been re-created, a synchronization on $ack$ is  possible
\begin{eqnarray*}
P_3 & \pired   &  (inc_0.(\out{r_0^\mathsf{S}}{\out{r_0^\mathsf{S}}{\encn{m_0}{0}} \parallel \choice{n_0}}) \, + \, dec_0.(\encn{m_0}{0})) \parallel \mathsf{REG}_0  \parallel \\ 
& & \overline{p_{i+1}} \parallel S = P_4
\end{eqnarray*}
Using the definition of $\encn{\cdot}{j}$ we note that $P_4$ actually corresponds to 
\[
P_4 = (inc_0.(\out{r_0^\mathsf{S}}{\encn{m_0+1}{0}} \, + \, dec_0.(\encn{m_0}{0})) \parallel \mathsf{REG}_0  \parallel \overline{p_{i+1}} \parallel S
\]
which in turn can be written as 
\[
P_4 =  \overline{p_{i+1}} \parallel \encp{r_0 = m_0+1}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel \prod^{n}_{l = 1} \encp{(l : I_l)}{\mms}
\]
which corresponds to the encoding of $\encp{(i+1,m_0+1,m_1)_N}{\mms}$, as desired.
\end{proof}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{mylem}\label{l:complete} 
Let $(i,m_0,m_1)$ be a configuration of a Minsky machine $N$. \\  %Consider a proceess $P = $.
If $\encp{(i,m_0,m_1)_N}{\mms}  \pired P_1$ then for every computation of $P_1$ there 
exists a $P_j$ such that 
%\begin{enumerate}
%\item $P_1 \pired \cdots \pired P_j$ 
%\item 
$P_j = \encp{(i',m'_0,m'_1)_N}{\mms}$ and
%\item 
$(i,m_0,m_1)\minskred (i',m'_0,m'_1)$.
%\end{enumerate}
\end{mylem}
 
\begin{proof}
Consider the reduction  $\encp{(i,m_0,m_1)_N}{\mms}  \pired P_1$. An analysis of the structure of process
 $\encp{(i,m_0,m_1)_N}{\mms}$ reveals that, in all cases, the only possibility for the first step corresponds to the
consumption of the program counter $p_i$. This implies that there exists an instruction
labeled with $i$, that can be executed from the configuration $(i,m_0,m_1)$.
%That is, there exists a configuration  $(i',m'_0,m'_1)$ such that  $(i,m_0,m_1) \minskred (i',m'_0,m'_1)$.
We proceed by a case analysis on the possible instruction, considering also the 
fact that the register on which the instruction acts can hold a value equal or greater than zero.
In all cases, it can be shown that computation evolves %(nearly) 
deterministically, 
until reaching a process in which a new program counter (that is, some $\overline{p_{i'}}$) appears.
% To be precise, there is 
% some non-determinism associated with the unfoldings of the encoding of recursive definitions
% (see Lemma \ref{l:corr-repl}).
% Since recursion is guarded, each recursive definition can be unfolded at most once, thus introducing at most a finite
% number of additional reductions. 
The program counter $\overline{p_{i'}}$ is inside a process that corresponds to $\encp{(i',m'_0,m'_1)_N}{\mms}$,
where $(i,m_0,m_1)\minskred (i',m'_0,m'_1)$. 
The analysis follows the same lines as the one reported for the proof of Lemma \ref{l:sound}, and we omit it.
\end{proof}

\begin{mylem}\label{l:terminate}
Let $N$ be a Minsky machine. We have that $N \nrightarrow_{M}$ if and only if $\encp{N}{\mms} \nrightarrow$.
\end{mylem}

\begin{proof}
Straightforward from Lemmas \ref{l:sound} and \ref{l:complete}.
\end{proof}

%\as{What's missing now is a proof of Lemma \ref{l:corr_minsky}, in particular the third point (which I believe is not a consequence of Lemma \ref{l:terminate}).}